B}' type is the type of functions with domain 'A'
and range type 'B(f,x)' on argument 'x', where 'f' is
the function itself. That is, this is a type of highly dependent functions,
whose range type depends on calls to the function itself. In this version,
the domain type 'A' must be well-founded with some relation 'R', and the calls
to the function in the range 'B' must always obey 'R'.
Here is a formal description of the type, along with its members.
We define '{f | x:A
B}' to be a type
with membership 'phi' iff
witthere is an 'alpha' such that
witther1. 'A' is a type with membership 'alpha'
witther2. 'A' is well-founded with respect to some partial order 'R'
witther3. for any 'a' such that 'alpha(a)'
witther3. there is a 'gamma_?' such that
witther3. therfor all 'b R a',
witther3. therfor 1. '{f | x:{c:A| c R b}
B}' is a type with membership 'gamma_b',
witther3. therfor 2. there is a 'beta_?' such that
witther3. therfor 2. t1. for any 'g' such that 'gamma_b(g)',
witther3. therfor 2. t1. for 'B(g,b)' is a type with membership 'beta_g'
witther3. therfor 2. t2. for any 'f', 'phi(f)' iff
witther3. therfor 2. t2. for for all 'a' such that 'alpha(a)', 'beta_a(f(a))'